(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, 1).
The TRS R consists of the following rules:
terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(n__add(sqr(activate(X)), dbl(activate(X))))
dbl(0) → 0
dbl(s(X)) → s(n__s(n__dbl(activate(X))))
add(0, X) → X
add(s(X), Y) → s(n__add(activate(X), Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(activate(X), activate(Z)))
terms(X) → n__terms(X)
add(X1, X2) → n__add(X1, X2)
s(X) → n__s(X)
dbl(X) → n__dbl(X)
first(X1, X2) → n__first(X1, X2)
activate(n__terms(X)) → terms(X)
activate(n__add(X1, X2)) → add(X1, X2)
activate(n__s(X)) → s(X)
activate(n__dbl(X)) → dbl(X)
activate(n__first(X1, X2)) → first(X1, X2)
activate(X) → X
Rewrite Strategy: INNERMOST
(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)
The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
sqr(s(X)) → s(n__add(sqr(activate(X)), dbl(activate(X))))
dbl(s(X)) → s(n__s(n__dbl(activate(X))))
add(s(X), Y) → s(n__add(activate(X), Y))
first(s(X), cons(Y, Z)) → cons(Y, n__first(activate(X), activate(Z)))
(2) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, 1).
The TRS R consists of the following rules:
dbl(0) → 0
terms(X) → n__terms(X)
terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
first(0, X) → nil
activate(n__add(X1, X2)) → add(X1, X2)
activate(n__dbl(X)) → dbl(X)
activate(X) → X
add(X1, X2) → n__add(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__terms(X)) → terms(X)
sqr(0) → 0
add(0, X) → X
first(X1, X2) → n__first(X1, X2)
dbl(X) → n__dbl(X)
s(X) → n__s(X)
activate(n__s(X)) → s(X)
Rewrite Strategy: INNERMOST
(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
dbl(0) → 0
dbl(z0) → n__dbl(z0)
terms(z0) → n__terms(z0)
terms(z0) → cons(recip(sqr(z0)), n__terms(s(z0)))
first(0, z0) → nil
first(z0, z1) → n__first(z0, z1)
activate(n__add(z0, z1)) → add(z0, z1)
activate(n__dbl(z0)) → dbl(z0)
activate(z0) → z0
activate(n__first(z0, z1)) → first(z0, z1)
activate(n__terms(z0)) → terms(z0)
activate(n__s(z0)) → s(z0)
add(z0, z1) → n__add(z0, z1)
add(0, z0) → z0
sqr(0) → 0
s(z0) → n__s(z0)
Tuples:
DBL(0) → c
DBL(z0) → c1
TERMS(z0) → c2
TERMS(z0) → c3(SQR(z0), S(z0))
FIRST(0, z0) → c4
FIRST(z0, z1) → c5
ACTIVATE(n__add(z0, z1)) → c6(ADD(z0, z1))
ACTIVATE(n__dbl(z0)) → c7(DBL(z0))
ACTIVATE(z0) → c8
ACTIVATE(n__first(z0, z1)) → c9(FIRST(z0, z1))
ACTIVATE(n__terms(z0)) → c10(TERMS(z0))
ACTIVATE(n__s(z0)) → c11(S(z0))
ADD(z0, z1) → c12
ADD(0, z0) → c13
SQR(0) → c14
S(z0) → c15
S tuples:
DBL(0) → c
DBL(z0) → c1
TERMS(z0) → c2
TERMS(z0) → c3(SQR(z0), S(z0))
FIRST(0, z0) → c4
FIRST(z0, z1) → c5
ACTIVATE(n__add(z0, z1)) → c6(ADD(z0, z1))
ACTIVATE(n__dbl(z0)) → c7(DBL(z0))
ACTIVATE(z0) → c8
ACTIVATE(n__first(z0, z1)) → c9(FIRST(z0, z1))
ACTIVATE(n__terms(z0)) → c10(TERMS(z0))
ACTIVATE(n__s(z0)) → c11(S(z0))
ADD(z0, z1) → c12
ADD(0, z0) → c13
SQR(0) → c14
S(z0) → c15
K tuples:none
Defined Rule Symbols:
dbl, terms, first, activate, add, sqr, s
Defined Pair Symbols:
DBL, TERMS, FIRST, ACTIVATE, ADD, SQR, S
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 16 trailing nodes:
ACTIVATE(n__s(z0)) → c11(S(z0))
ACTIVATE(n__dbl(z0)) → c7(DBL(z0))
ACTIVATE(n__first(z0, z1)) → c9(FIRST(z0, z1))
ACTIVATE(n__terms(z0)) → c10(TERMS(z0))
FIRST(z0, z1) → c5
DBL(z0) → c1
FIRST(0, z0) → c4
TERMS(z0) → c2
ADD(0, z0) → c13
ACTIVATE(n__add(z0, z1)) → c6(ADD(z0, z1))
S(z0) → c15
SQR(0) → c14
ACTIVATE(z0) → c8
ADD(z0, z1) → c12
TERMS(z0) → c3(SQR(z0), S(z0))
DBL(0) → c
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
dbl(0) → 0
dbl(z0) → n__dbl(z0)
terms(z0) → n__terms(z0)
terms(z0) → cons(recip(sqr(z0)), n__terms(s(z0)))
first(0, z0) → nil
first(z0, z1) → n__first(z0, z1)
activate(n__add(z0, z1)) → add(z0, z1)
activate(n__dbl(z0)) → dbl(z0)
activate(z0) → z0
activate(n__first(z0, z1)) → first(z0, z1)
activate(n__terms(z0)) → terms(z0)
activate(n__s(z0)) → s(z0)
add(z0, z1) → n__add(z0, z1)
add(0, z0) → z0
sqr(0) → 0
s(z0) → n__s(z0)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
dbl, terms, first, activate, add, sqr, s
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(8) BOUNDS(1, 1)